perm filename BLISET.AX[226,JMC] blob sn#005398 filedate 1972-06-18 generic text, type T, neo UTF8
00100	GIVEAX(SITDEF,(∀ S)(∀ Y)(∀ X)(X ε SIT(Y,S) ≡ SITTING(X,Y,S)));
00200	
00300	GIVEAX(SITSET,(∀ S)(∀ Y)(ISSET SIT(Y,S)));
00400	
00500	GIVEAX(EXTENSIONALITY,(∀ U)(∀ V)(ISSET U ∧ ISSET V ⊃
00600		((∀ X)(XεU ≡ XεV) ⊃ U=V)));
00700	
00800	GIVEAX(SITTING,(∀ S)(∀ X)(∀ Y)(SITTING(X,Y,S) ≡
00900		(AT(X,Y,S)∧¬(X=ROBOT)∧¬HOLDING(X,S))));
01000	
01100	GIVEAX(HELDSET,(∀ S)(ISSET HELD S));
01200	
01300	GIVEAX(HELDDEF, (∀ S)(∀ X)(HOLDING(X,S)⊃HELD(S)=UNITSET(X)));
01400	
01500	GIVEAX(HELDDEF2,(∀ S)((∀ X)(¬HOLDING(X,S))⊃(HELD(S)=NULLSET)));
01600	
01700	GIVEAX(NULLSET,ISSET NULLSET);
01800	
01900	GIVEAX(NULL1,(∀ X)(¬(XεNULLSET)));
02000	
02100	GIVEAX(UNITSET,(∀ X)(∀ Y)(YεUNITSET(X)≡(Y=X)));
02200	
02300	GIVEAX(UNIONSET,(∀ X)(∀ Y)(ISSET X ∧ ISSET Y ⊃ ISSET UNION(X,Y)));
02400	
02500	GIVEAX(UNION,(∀ X)(∀ Y)(∀ Z)(ZεUNION(X,Y)≡ZεX∨ZεY));
02600	
02700	END;